Veloso-Pereira-Haeusler_On-what-there-must-be.

"Dieser Band zu Hegels 'Enzyklopädie der philosophischen Wissenschaften' (1830) ist Teil eines dreibändigen Kommentars zu Hegels Hauptwerken. Es ist das Ziel dieser Kommentare, Hegels philosophisches Werk einem breiteren Lesepublikum zu erschliessen. Sie wollen die selbständige Lektüre der meist sehr schwierigen Hegel-Texte nicht durch referierende Darstellung ersetzen, sondern sie gerade ermöglichen - durch textnahe Erläuterungen, systematische Begriffsklärungen und den Aufweis von inhaltlichen Querverbindungen im Riesengebäude des Hegelschen Werkes. Auch die philosophie- und wissenschaftsgeschichtlichen Zusammenhänge, in denen Hegels System entsteht und Struktur gewinnt, (...) werden herausgestellt. Alle Autoren, die sich an diesem Projekt beteiligen, sind in der Hegelforschung und -interpretation durch eigene Beiträge bestens ausgewiesen, so das ihre Kommentare beanspruchen dürfen, auch hier 'auf dem neusten Stand' zu sein. Vor allem aber soll Hegel selbst zu Wort kommen und dabei nicht nur gehört, sondern auch verstanden werden."--. (shrink)

Spatial region concepts such as “front,” “back,” “left,” and “right” reflect our typical interaction with space, and the corresponding surrounding regions have different statuses in memory. We examined the representation of spatial directions in the auditory space, specifically in how far natural response actions, such as orientation movements toward a sound source, would affect the categorization of egocentric auditory space. While standing in the middle of a circle with 16 loudspeakers, participants were presented acoustic stimuli coming from the loudspeakers in (...) randomized order, and verbally described their directions by using the concept labels “front,” “back,” “left,” “right,” “front-right,” “front-left,” “back-right,” and “back-left.” Response actions varied in three blocked conditions: (1) facing front, (2) turning the head and upper body to face the stimulus, and (3) turning the head and upper body plus pointing with the hand and outstretched arm toward the stimulus. In addition to a protocol of the verbal utterances, motion capture and video recording generated a detailed corpus for subsequent analysis of the participants’ behavior. Chi-square tests revealed an effect of response condition for directions within the left and right sides. We conclude that movement-based response actions influence the representation of auditory space, especially within the sides’ regions. Moreover, the representation of auditory space favors the front and the back regions in terms of resolution, which is possibly related to the physiological characteristics of the human auditory system, as well as to the ecological requirements of action control in the different regions. (shrink)

Sambin [6] proved the normalization theorem for GL, the modal logic of provability, in a sequent calculus version called by him GLS. His proof does not take into account the concept of reduction, commonly used in normalization proofs. Bellini [1], on the other hand, gave a normalization proof for GL using reductions. Indeed, Sambin's proof is a decision procedure which builds cut-free proofs. In this work we formalize this procedure as a recursive function and prove its recursiveness in an arithmetically (...) formalizable way, concluding that the normalization of GL can be formalized in PA. MSC: 03F05, 03B35, 03B45. (shrink)

The relation between ex falso and disjunctive syllogism, or even the justification of ex falso based on disjunctive syllogism, is an old topic in the history of logic. This old topic reappears in contemporary logic since the introduction of minimal logic by Johansson. The disjunctive syllogism seems to be part of our general non-problematic inferential practices and superficially it does not seem to be related to or to depend on our acceptance of the frequently disputable ex falso rule. We know (...) that the acceptance of the ex falso is a sufficient condition for the acceptance of the disjunctive syllogism, but the interesting question is: is the ex falso a necessary condition for the acceptance of the disjunctive syllogism? The aim of the present paper is to discuss some possible ways to define systems that combines the preservation of the disjunctive syllogism with the rejection of the ex falso. (shrink)

This collection of papers, celebrating the contributions of Swedish logician Dag Prawitz to Proof Theory, has been assembled from those presented at the Natural Deduction conference organized in Rio de Janeiro to honour his seminal research. Dag Prawitz’s work forms the basis of intuitionistic type theory and his inversion principle constitutes the foundation of most modern accounts of proof-theoretic semantics in Logic, Linguistics and Theoretical Computer Science. The range of contributions includes material on the extension of natural deduction with higher-order (...) rules, as opposed to higher-order connectives, and a paper discussing the application of natural deduction rules to dealing with equality in predicate calculus. The volume continues with a key chapter summarizing work on the extension of the Curry-Howard isomorphism, via methods of category theory that have been successfully applied to linear logic, as well as many other contributions from highly regarded authorities. With an illustrious group of contributors addressing a wealth of topics and applications, this volume is a valuable addition to the libraries of academics in the multiple disciplines whose development has been given added scope by the methodologies supplied by natural deduction. The volume is representative of the rich and varied directions that Prawitz work has inspired in the area of natural deduction. (shrink)

We upgrade [3] to a complete proof of the conjecture NP = PSPACE that is known as one of the fundamental open problems in the mathematical theory of computational complexity; this proof is based on [2]. Since minimal propositional logic is known to be PSPACE complete, while PSPACE to include NP, it suffices to show that every valid purely implicational formula ρ has a proof whose weight and time complexity of the provability involved are both polynomial in the weight of (...) ρ. As is [3], we use proof theoretic approach. Recall that in [3] we considered any valid ρ in question that had a “short” tree-like proof π in the Hudelmaier-style cutfree sequent calculus for minimal logic. The “shortness” means that the height of π and the total weight of different formulas occurring in it are both polynomial in the weight of ρ. However, the size, and hence also the weight, of π could be exponential in that of ρ. To overcome this trouble we embedded π into Prawitz’s proof system of natural deductions containing single formulas, instead of sequents. As in π, the height and the total weight of different formulas of the resulting tree-like natural deduction ∂1 were polynomial, although the size of ∂1 still could be exponential, in the weight of ρ. In our next, crucial move, ∂1 was deterministically compressed into a “small”, although multipremise, dag-like deduction ∂ whose horizontal levels contained only mutually different formulas, which made the whole weight polynomial in that of ρ. However, ∂ required a more complicated verification of the underlying provability of ρ. In this paper we present a nondeterministic compression of ∂ into a desired standard dag-like deduction ∂0 that deterministically proves ρ in time and space polynomial in the weight of ρ.2 Together with [3] this completes the proof of NP = PSPACE.Natural deductions are essential for our proof. Tree-to-dag horizontal compression of π merging equal sequents, instead of formulas, is not sufficient, since the total number of different sequents in π might be exponential in the weight of ρ – even assuming that all formulas occurring in sequents are subformulas of ρ. On the other hand, we need Hudelmaier’s cutfree sequent calculus in order to control both the height and total weight of different formulas of the initial tree-like proof π, since standard Prawitz’s normalization although providing natural deductions with the subformula property does not preserve polynomial heights. It is not clear yet if we can omit references to π even in the proof of the weaker result NP = coNP. (shrink)

We present a categorical/denotational semantics for the Lambek Syntactic Calculus , indeed for a λlD-typed version Curry-Howard isomorphic to it. The main novelty of our approach is an abstract noncommutative construction with right and left adjoints, called sequential product. It is defined through a hierarchical structure of categories reflecting the implicit permission to sequence expressions and the inductive construction of compound expressions. We claim that Lambek's noncommutative product corresponds to a noncommutative bi-endofunctor into a category, which encloses all categories of (...) such hierarchical structure. A soundness theorem for LSC is shown with respect to this semantical framework. (shrink)

In our previous work we proved the conjecture NP = PSPACE by advanced proof theoretic methods that combined Hudelmaier’s cut-free sequent calculus for minimal logic with the horizontal compressing in the corresponding minimal Prawitz-style natural deduction. In this Addendum we show how to prove a weaker result NP = coNP without referring to HSC. The underlying idea is to omit full minimal logic and compress only “naive” normal tree-like ND refutations of the existence of Hamiltonian cycles in given non-Hamiltonian graphs, (...) since the Hamiltonian graph problem in NPcomplete. Thus, loosely speaking, the proof of NP = coNP can be obtained by HSC-elimination from our proof of NP = PSPACE. (shrink)

We show that arbitrary tautologies of Johansson’s minimal propositional logic are provable by “small” polynomial-size dag-like natural deductions in Prawitz’s system for minimal propositional logic. These “small” deductions arise from standard “large” tree-like inputs by horizontal dag-like compression that is obtained by merging distinct nodes labeled with identical formulas occurring in horizontal sections of deductions involved. The underlying geometric idea: if the height, h(∂), and the total number of distinct formulas, ϕ(∂), of a given tree-like deduction ∂ of a minimal (...) tautology ρ are both polynomial in the length of ρ, |ρ|, then the size of the horizontal dag-like compression ∂ᶜ is at most h(∂)×ϕ(∂), and hence polynomial in |ρ|. That minimal tautologies ρ are provable by tree-like natural deductions ∂ with |ρ|-polynomial h(∂) and ϕ(∂) follows via embedding from Hudelmaier’s result that there are analogous sequent calculus deductions of sequent ⇒ρ. The notion of dag-like provability involved is more sophisticated than Prawitz’s tree-like one and its complexity is not clear yet. Our approach nevertheless provides a convergent sequence of NP lower approximations of PSPACE-complete validity of minimal logic. (shrink)

This paper is a continuation of dag-like proof compression research initiated in [9]. We investigate proof compression phenomenon in a particular, most transparent case of propositional DNF Logic. We define and analyze a very efficient semi-analytic sequent calculus SEQ*0 for propositional DNF. The efficiency is achieved by adding two special rules CQ and CS; the latter rule is a variant of the weakened substitution rule WS from [9], while the former one being specially designed for DNF sequents. We show that (...) dag-like SEQ*0 has good deterministic proof search strategy. Furthermore, we expose six examples showing that dag-like deducibility in SEQ*0 admits exponential-size proof compression, as compared to familiar proof systems like cutfree sequent calculi, resolution and cutting plane proof systems. (shrink)

Economic growth and development remain embedded in the very core of our current international economic system and the so called “material economy”. However, depleting natural resources and environmental degradation, which now threaten the well-being of future generations, has challenged this premise, and placed sustainable development as a necessary objective of business activity and expansion. Environmental impact assessments (EIAs) have emerged as a key tool for governments, businesses, and NGOs to manage the negative impact of their activities on the environment. Businesses (...) in particular play a key role in averting or mitigating current environmental trends given that the economic growth they have stimulated has serious consequences for both the environment and social well-being. However, research on the use of EIAs has been conducted mostly from a governmental perspective producing a clear gap between research development and business (corporate) practice. To bridge this gap in knowledge, we develop a new EIA process tailored to real world business constraints and provide a range of propositions which we hope will stimulate future research efforts toward understanding and guiding how businesses integrate environmental issues into their decision-making processes. (shrink)

Last October the German Ambassador to Britain delivered the annual Gresham Special Lecture in Gresham College in the City of London. The text of His Excellency's lecture is reproduced here with permission.

Last October the German Ambassador to Britain delivered the annual Gresham Special Lecture in Gresham College in the City of London. The text of His Excellency's lecture is reproduced here with permission.

Der Kinder- und Jugendgesundheitssurvey soll repräsentative, gültige Daten und Erkenntnisse zur gesundheitlichen Situation von Kindern und Jugendlichen in Deutschland als entscheidende Voraussetzung für die Bewertung und die Verbesserung von deren gesundheitlicher Lage schaffen. Forschung und insbesondere Blutentnahmen an nichteinwilligungsfähigen Personen erfordern eine profunde ethische und rechtliche Überprüfung. Der Beitrag befasst sich damit, welche medizinethischen Empfehlungen und welche rechtlichen Grundsätze in Deutschland für die Bewertung relevant sind. Nach geltendem deutschen Recht können Eltern zu Blutentnahmen bei ihren Kindern nur zustimmen, wenn diese (...) in deren individuellem gesundheitlichen Interesse liegen. Ein „gruppenspezifischer Nutzen“, wie er von Medizinethikern national und international als Voraussetzung für ethische Akzeptabilität (bei minimalem Risiko der Untersuchungen) ebenfalls für sinnvoll und wichtig angesehen wird, und der in dem geplanten Survey in jedem Falle gegeben wäre, genügt deutschen Rechtsansprüchen nicht. Im Pretest hat sich der potenzielle individuelle Nutzen der Blutentnahmen bestätigt: Viele Kinder hatten biochemisch nachweisbare Gesundheitsrisiken (z. B. verborgener Nährstoffmangel, allergische Sensibilisierung, Hinweise auf Impflücken oder langfristige Gesundheitsrisiken), die ohne Blutuntersuchung nicht feststellbar gewesen wären. Bei über 90% der Kinder waren nach schriftlicher Einwilligung der Eltern und Jugendlichen sowie informeller Zustimmung der Kinder, die in jedem einzelnen Falle berücksichtigt wurde, Blutentnahmen möglich. Nach der Befragung einer Unterstichprobe ist die Akzeptanz insgesamt gut. (shrink)

The introduction and elimination rules for material implication in natural deduction are not complete with respect to the implicational fragment of classical logic. A natural way to complete the system is through the addition of a new natural deduction rule corresponding to Peirce's formula → A) → A). E. Zimmermann [6] has shown how to extend Prawitz' normalization strategy to Peirce's rule: applications of Peirce's rule can be restricted to atomic conclusions. The aim of the present paper is to extend (...) Seldin's normalization strategy to Peirce's rule by showing that every derivation Π in the implicational fragment can be transformed into a derivation Π' such that no application of Peirce's rule in Π' occurs above applications of →-introduction and →-elimination. As a corollary of Seldin's normalization strategy we obtain a form of Glivenko's theorem for the classical {→}-fragment. (shrink)